| Definitions | P & Q,  x:A. B(x), t  T, P   Q, 2of(t), f(a), <a,b>, Type, s = t,  b, f(x), x dom(f), f || g, x : v, x:A B(x), a:A fp B(a), 1of(t), Knd, type List, x:A B(x), #$n, a<b, Void, False,  A, A B,  , {x:A| B(x) },  , Atom, Id, left+right,  x:A. B(x), Top, IdLnk, Case b of inl(x) s(x) ; inr(y) t(y), if b t else f fi,  x.A(x),  x. t(x), map(f;as), (x l), P  Q, IdLnkDeq, KindDeq, product-deq(A;B;a;b), Prop, eqof(d), false, IdDeq, P  Q, P Q, p q, nil, M.state, M.da(a), (s1  s2 mod x), {i..j }, M.dout(l,tg), f(x)?z,  , locl(a), car.cdr, xdom(f). v=f(x) P(x;v), z != f(x) P(a;z), M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), ma-frame-compatible(A;B), mk-ma, , with declarations ds:dsda:dak(v) sends f s v on link l, (with ds: ds action a:T precondition a(v) is P s v), deq-member(eq;x;L), A & B, f  g, State(ds), Valtype(da;k), rcv(l,tg), M1 ||decl M2, M1 || M2, A ||+ B |
f:(Id